STM: ite false

STM: iflift 1

STM: iflift sq 1

STM: cand functionality wrt iff

STM: trivial ite 2

STM: ite and reduce

ABS: x,y,z. t(x;y;z)

ABS: x,y,z,w. t(x;y;z;w)

ABS: x,y,z,w,v. t(x;y;z;w;v)

ABS: x,y,z,u,v,w. t(x;y;z;u;v;w)

STM: select cons tl sq

ABS: HIDDEN

STM: hide wf

ABS: x  {FDLNOr10865}

ABS: !x:T. P(x)

STM: exists! wf

ABS: (b?x)

STM: opt wf

ABS: T1  T2

STM: isect2 wf

STM: isect2 decomp

STM: isect prod lemma

ABS: Decision

STM: decision wf

ABS: dec2bool(d)

STM: dec2bool wf

STM: inr eq bfalse

STM: inl eq btrue

STM: bool decision

STM: inr wf

STM: comb for inr wf

STM: inl wf

STM: comb for inl wf

STM: decidable decision

STM: dec2bool decidable

STM: eqtt assert 2

STM: eqff assert 2

STM: assert dec2bool

ABS: increasing(f;k)

STM: increasing wf

STM: decidable cand

STM: subtype top